$\forall$$A$:Type, ${\it eq}$:EqDecider($A$), $B$:($A$$\rightarrow$Type), $P$:($A$$\rightarrow\mathbb{B}$), $f$:$x$:$A$ fp$\rightarrow$ $B$($x$), $a$:$A$.
\\[0ex]($\uparrow$$a$ $\in$ dom($f$))
\\[0ex]$\Rightarrow$ ($\forall$$b$:$A$. ($\uparrow$($P$($b$))) $\Leftarrow\!\Rightarrow$ ($b$ = $a$))
\\[0ex]$\Rightarrow$ (fpf{-}vals(${\it eq}$;$P$;$f$) = [$<$$a$, $f$($a$)$>$] $\in$ (($x$:$A$ $\times$ $B$($x$)) List))